1. Technical Field
The present invention relates to computer program verification and more particularly to systems and methods for detecting data races in concurrent programs using asynchronous calls.
2. Description of the Related Art
Real-life concurrent programs often are based on an event-driven model where threads create tasks and dispatch these tasks to other threads, to be executed asynchronously. The tasks are queued on to a work queue of the other threads and are processed by the corresponding schedulers in an iterative fashion. This model combines the expressiveness of both thread and event-based models of computation, and has the advantage that the thread that creates the task may not wait for the task to finish.
Threads can delegate computationally intensive tasks to other threads while continuing with more immediate tasks. Several large industrial concurrent systems including Ajax-based scripts, routers, and web servers use this paradigm of concurrent computation.
Although providing much flexibility to a system designer and superior run-time performance, multi-threaded programs with asynchronous events are extremely hard to debug and verify. First, there is a loose correlation between the asynchronous call and the value returned making it difficult to track the flow of data across threads. More significantly, these calls are often made using function pointers, and arguments to these calls, in turn, contain function pointers to callback functions, which are executed, for example, upon completion of the call. Such indirect mechanisms for communication among threads make analysis of these programs extremely tricky. For example, the values of the function pointers passed into indirect calls depend on the particular calling context and therefore must be tracked context-sensitively.